Inference at * 
Iof proof for Lemma mu' wf:


  A:Type, P:(A), d:(x:A. Dec(n:. ((P(x,n))))). mu'(P)  A( + Top) 

latex

 by ((Auto) 
CollapseTHEN (Unfold `mu\'` 
0)) 
0CollapseTHEN (Subst' 
0CTERMOF{p-mu-decider:ObjectId, 1:l, 1:l} ~ TERMOF{p-mu-decider:ObjectId, 1:l, i:l} ( 0)) 

latex

0C1: .....equality..... NILNIL

0C1: 1. A : Type
0C1: 2. P : A
0C1: 3. x:A. Dec(n:. ((P(x,n))))
0C1:   TERMOF{p-mu-decider:ObjectId, 1:l, 1:l} ~ TERMOF{p-mu-decider:ObjectId, 1:l, i:l}
0C2: 

0C2: 1. A : Type
0C2: 2. P : A
0C2: 3. d : x:A. Dec(n:. ((P(x,n))))
0C2:   (x.(TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1)  A( + Top)
0C.

Definitions

s ~ t, p-mu-decider, Type, , Dec(P), x:A. B(x), x:A  B(x), b, x:A. B(x), x:AB(x), left + right, , Top, t  T, mu'(P)